Nuprl Lemma : bimplies_transitivity
9,38
postcript
pdf
u
,
v
,
w
:
. (
(
u
v
))
(
(
v
w
))
(
(
u
w
))
latex
ProofTree
Definitions
ff
,
t
T
,
True
,
if
b
then
t
else
f
fi
,
tt
,
b
,
P
Q
,
False
,
Lemmas
bool
wf
,
false
wf
,
true
wf
origin
u,v,w:
. (
(u 
v)) ((v w)) ((u w))
u,v,w:. ((u v)) ((v w)) ((u w))
Tb Q